|
| 1: |
|
eq(0,0) |
→ true |
| 2: |
|
eq(0,s(x)) |
→ false |
| 3: |
|
eq(s(x),0) |
→ false |
| 4: |
|
eq(s(x),s(y)) |
→ eq(x,y) |
| 5: |
|
or(true,y) |
→ true |
| 6: |
|
or(false,y) |
→ y |
| 7: |
|
union(empty,h) |
→ h |
| 8: |
|
union(edge(x,y,i),h) |
→ edge(x,y,union(i,h)) |
| 9: |
|
reach(x,y,empty,h) |
→ false |
| 10: |
|
reach(x,y,edge(u,v,i),h) |
→ if_reach_1(eq(x,u),x,y,edge(u,v,i),h) |
| 11: |
|
if_reach_1(true,x,y,edge(u,v,i),h) |
→ if_reach_2(eq(y,v),x,y,edge(u,v,i),h) |
| 12: |
|
if_reach_2(true,x,y,edge(u,v,i),h) |
→ true |
| 13: |
|
if_reach_2(false,x,y,edge(u,v,i),h) |
→ or(reach(x,y,i,h),reach(v,y,union(i,h),empty)) |
| 14: |
|
if_reach_1(false,x,y,edge(u,v,i),h) |
→ reach(x,y,i,edge(u,v,h)) |
|
There are 11 dependency pairs:
|
| 15: |
|
EQ(s(x),s(y)) |
→ EQ(x,y) |
| 16: |
|
UNION(edge(x,y,i),h) |
→ UNION(i,h) |
| 17: |
|
REACH(x,y,edge(u,v,i),h) |
→ IF_REACH_1(eq(x,u),x,y,edge(u,v,i),h) |
| 18: |
|
REACH(x,y,edge(u,v,i),h) |
→ EQ(x,u) |
| 19: |
|
IF_REACH_1(true,x,y,edge(u,v,i),h) |
→ IF_REACH_2(eq(y,v),x,y,edge(u,v,i),h) |
| 20: |
|
IF_REACH_1(true,x,y,edge(u,v,i),h) |
→ EQ(y,v) |
| 21: |
|
IF_REACH_2(false,x,y,edge(u,v,i),h) |
→ OR(reach(x,y,i,h),reach(v,y,union(i,h),empty)) |
| 22: |
|
IF_REACH_2(false,x,y,edge(u,v,i),h) |
→ REACH(x,y,i,h) |
| 23: |
|
IF_REACH_2(false,x,y,edge(u,v,i),h) |
→ REACH(v,y,union(i,h),empty) |
| 24: |
|
IF_REACH_2(false,x,y,edge(u,v,i),h) |
→ UNION(i,h) |
| 25: |
|
IF_REACH_1(false,x,y,edge(u,v,i),h) |
→ REACH(x,y,i,edge(u,v,h)) |
|
The approximated dependency graph contains 3 SCCs:
{15},
{16}
and {17,19,22,23,25}.